Step of Proof: dec_iff_ex_bvfun
12,41
postcript
pdf
Inference at
*
1
1
1
1
1
I
of proof for Lemma
dec
iff
ex
bvfun
:
1.
T
: Type
2.
E
:
T
T
3.
g
:
x
:
T
y
:
T
. (
E
(
x
,
y
))
(
(
E
(
x
,
y
)))
4.
x
:
T
5.
y
:
T
6.
y1
:
y
:
T
(
E
(
x
,
y
))
(
(
E
(
x
,
y
)))
7.
y1
=
g
(
x
)
8.
y2
: (
E
(
x
,
y
))
(
(
E
(
x
,
y
)))
9.
y2
=
y1
(
y
)
(
case
g
(
x
,
y
) of inl(
a
) => tt | inr(
b
) => ff)
(
E
(
x
,
y
))
latex
by D 8
latex
1
:
1:
8.
x1
:
E
(
x
,
y
)
1:
9. (inl
x1
) =
y1
(
y
)
1:
(
case
g
(
x
,
y
) of inl(
a
) => tt | inr(
b
) => ff)
(
E
(
x
,
y
))
2
:
2:
8.
y3
:
(
E
(
x
,
y
))
2:
9. (inr
y3
) =
y1
(
y
)
2:
(
case
g
(
x
,
y
) of inl(
a
) => tt | inr(
b
) => ff)
(
E
(
x
,
y
))
.
Definitions
P
Q
origin